package ADTs;

import java.awt.event.KeyEvent;
import java.io.Serializable;
import java.util.ArrayList;

import Project.SaveFile;


/**
 * This class is a data structure of a file.
 * Its constructor contains all kinds of default values such as
 * number of levels beaten, initial money, default control and
 * weapon upgrade status. Also this data structure can store
 * 
 * @author	Brian Wetherbee
 * 			Ryan McNamara
 * 			Zeng Yang
 *
 */
public class FileADT implements Serializable{
	
	
	//initial money value.
	public static final int STARTING_MONEY = 100000;
	//@ requires money == 0;
	//@ ensures levelsBeaten == 0;
	//@ ensures money == STARTING_MONEY;
	//@ ensures fileNo == SaveFile.getNumberOfFiles();
	public FileADT(){
		money = STARTING_MONEY;
		levelsBeaten = 0;
		fileNo = SaveFile.getNumberOfFiles();
		
		ArrayList<ArrayList<Integer>> toAdd = new ArrayList<ArrayList<Integer>>(3);
		for(int index = 0; index < 3; index++) {
			ArrayList<Integer> index0 = new ArrayList<Integer>();
			index0.add(0);
			index0.add(0);
			index0.add(0);
			
			toAdd.add(index0);
		}
		
		setWeaponUpgradeStatus(toAdd);
		
		//default controls		
		controlUp = java.awt.event.KeyEvent.VK_W;
		controlDown = java.awt.event.KeyEvent.VK_S;
		controlLeft = java.awt.event.KeyEvent.VK_A;
		controlRight = java.awt.event.KeyEvent.VK_D;
		controlConfirm = java.awt.event.KeyEvent.VK_ENTER;
		controlCancel = java.awt.event.KeyEvent.VK_BACK_SPACE;
		controlQuit = java.awt.event.KeyEvent.VK_ESCAPE;
		controlUpgrade = java.awt.event.KeyEvent.VK_Q;
		controlCustomize = java.awt.event.KeyEvent.VK_E;
		controlToggleFullScreen = KeyEvent.VK_F12;
	}

	//@ public invariant money >= 0;
	//@ public invariant weaponUpgradeStatus.size() == Constants.MAX_UPGRADE_STATUS.size();
	/*@ public invariant 	(\forall int i;
	                     	0 <= i && i < weaponUpgradeStatus.size();
	   							weaponUpgradeStatus.get(i).size() == Constants.MAX_UPGRADE_STATUS.get(i).size() &&
	                     		(\forall int j;
	    						0 <= j && j < weaponUpgradeStatus.get(i).size();
	    						0<= weaponUpgradeStatus.get(i).get(j) 
	    						&& weaponUpgradeStatus.get(i).get(j) <= Constants.MAX_UPGRADE_STATUS.get(i).get(j)
	    						)
	    					)
		@*/
	private /*@spec_public@*/double money;
	private /*@spec_public@*/int levelsBeaten;
	//weaponUpgradeStatus.get(0) = Machine Gun
	//weaponUpgradeStatus.get(1) = ...
	//weaponUpgradeStatus.get(2) = ...
	private /*@spec_public@*/ArrayList<ArrayList<Integer>> weaponUpgradeStatus;
	private int fileNo;

	//Instance variables of controls
	public int controlUp;
	public int controlDown;
	public int controlLeft;
	public int controlRight;
	public int controlConfirm;
	public int controlCancel;
	public int controlQuit;
	public int controlUpgrade;
	public int controlCustomize;
	public int controlToggleFullScreen;
	
	
	/*@ requires true 
	  @*/
	public boolean equals(FileADT file) {
		return false;
	}

	//@ ensures this.money == money;
	public void setMoney(double money) {
		this.money = money;
	}
	//@ ensures \result == money;
	public double getMoney() {
		return money;
	}
	
	//@ ensures this.levelsBeaten == levelsBeaten;
	public void setLevelsBeaten(int levelsBeaten) {
		this.levelsBeaten = levelsBeaten;
	}

	//@ ensures \result == levelsBeaten;
	public int getLevelsBeaten() {
		return levelsBeaten;
	}
	
	//@ requires levelsBeaten >= 0;
	//@ ensures levelsBeaten == (\old levelsBeaten + 1);
	//@ ensures levelsBeaten <= 27;
	public void incrementLevelsBeaten(){
		levelsBeaten++;
	}

	//@ requires weaponUpgradeStatus != null;
	//@ requires weaponUpgradeStatus >= 1;
	/*@ ensures (\forall int i; 0 <=i && i < weaponUpgradeStatus.size(); 
				this.weaponUpgradeStatus.get(i).equals(weaponUpgradeStatus.get(i)));
				@*/
	public void setWeaponUpgradeStatus(ArrayList<ArrayList<Integer>> weaponUpgradeStatus) {
		this.weaponUpgradeStatus = weaponUpgradeStatus;
	}

	//@ ensures \result == weaponUpgradeStatus; 
	public ArrayList<ArrayList<Integer>> getWeaponUpgradeStatus() {
		return weaponUpgradeStatus;
	}
	//@ requires fileNo >= 0;
	//@ ensures this.fileNo == fileNo;
	public void setFileNo(int fileNo) {
		this.fileNo = fileNo;
	}

	//@ ensures \result == fileNo; 
	public int getFileNo() {
		return fileNo;
	}
}
